Publication Details
Andrey Chernikov and Jing Xu.
Published in Computational Geometry: Theory and Applications, Publisher Elsevier, March, 2015
Abstract
The Marching Cubes algorithm is a well known and widely used approach for extracting a triangulated isosurface from a three-dimensional rectilinear grid of uniformly sampled data values. The algorithm relies on a large manually constructed table which exhaustively enumerates all possible patterns in which the isovalue relates to the values in the nodes of a cubical cell of the grid. For each pattern the table contains the local connectivity of the triangles. The construction of this table is labor intensive and error prone. Indeed, the original paper allowed for topological holes in the surface. This problem was later fixed by several authors, however a proof of correctness to our knowledge was never presented. Another issue, the possibility of intersecting triangles inside a single cube, has not been addressed. In this paper we present our formal proof of correctness of a Marching Cubes implementation with respect to both of these conditions. Our proof is developed with the Coq proof assistant, and the script is available online.
